Subobject classifiers #802

maybemabeline · 2023-09-28T14:26:11Z

I plan to implement subobject classifiers, construct them in the category of presheaves and prove some adjacent results.
To start off I realized I need pullbacks in large precategories, so I tried enlarging the file. The object w' in line 123 is forced to be at level l1 by the following functions though and I can't seem to tell why. I also added the type of all monomorphisms in a large precategory.

src/category-theory/monomorphisms-in-large-precategories.lagda.md

src/category-theory/pullbacks-in-large-precategories.lagda.md

fredrik-bakke · 2023-09-28T14:45:25Z

src/category-theory/pullbacks-in-large-precategories.lagda.md

+
+## Idea
+
+A pullback of two morphisms `f : hom y x` and `g : hom z x` in a category `C`


Suggested change

A pullback of two morphisms `f : hom y x` and `g : hom z x` in a category `C`

A **pullback** of two morphisms `f : hom y x` and `g : hom z x` in a [category](category-theory.categories.md) `C`

We write terms in boldface when defining them, and add links when mentioning terms for the first time in a file that are defined elsewhere.

fredrik-bakke · 2023-09-28T14:46:01Z

src/category-theory/pullbacks-in-large-precategories.lagda.md

+- `p₁ ∘ h = p₁'`
+- `p₂ ∘ h = p₂'`.
+
+We say that `C` has all pullbacks if there is a choice of a pullback for each


Suggested change

We say that `C` has all pullbacks if there is a choice of a pullback for each

We say that `C` **has all pullbacks** if there is a choice of a pullback for each

fredrik-bakke · 2023-09-28T14:47:20Z

src/category-theory/pullbacks-in-large-precategories.lagda.md

+  (x : obj-Large-Precategory C l1)
+  (y : obj-Large-Precategory C l2)
+  (z : obj-Large-Precategory C l3)
+  (f : hom-Large-Precategory C y x)
+  (g : hom-Large-Precategory C z x)
+  (w : obj-Large-Precategory C l4)


You probably want x y z and w to be implicit arguments here, unless Agda is unable to infer them generally

Good point! I'll change this in the other file too.

Also, when they are implicit, I would place w right after z instead

src/category-theory/pullbacks-in-large-precategories.lagda.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

fredrik-bakke · 2023-09-28T14:56:10Z

src/category-theory/pullbacks-in-large-precategories.lagda.md

+    Σ (obj-Large-Precategory C l4) λ w →
+    Σ (hom-Large-Precategory C w y) λ p₁ →
+    Σ (hom-Large-Precategory C w z) λ p₂ →
+    Σ (comp-hom-Large-Precategory C f p₁
+    ＝ comp-hom-Large-Precategory C g p₂) λ α →
+      is-pullback-Large-Precategory x y z f g w p₁ p₂ α


The proper formatting for this is

Suggested change

Σ (obj-Large-Precategory C l4) λ w →

Σ (hom-Large-Precategory C w y) λ p₁ →

Σ (hom-Large-Precategory C w z) λ p₂ →

Σ (comp-hom-Large-Precategory C f p₁

＝ comp-hom-Large-Precategory C g p₂) λ α →

is-pullback-Large-Precategory x y z f g w p₁ p₂ α

Σ ( obj-Large-Precategory C l4)

( λ w →

Σ ( hom-Large-Precategory C w y)

( λ p →

Σ ( hom-Large-Precategory C w z)

( λ q →

Σ ( comp-hom-Large-Precategory C f p ＝

comp-hom-Large-Precategory C g q)

( is-pullback-Large-Precategory x y z f g w p q))))

(if that stays within the 80-character limit)

fredrik-bakke · 2023-09-28T15:01:19Z

src/category-theory/pullbacks-in-large-precategories.lagda.md

+    morphism-into-pullback-Large-Precategory :
+      hom-Large-Precategory C w' object-pullback-Large-Precategory
+    morphism-into-pullback-Large-Precategory =
+      pr1 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))


You will want to define named projections for things like this instead of using cryptic composites of pr1 and pr2. Maybe a good reference for how to do this is to look at how we define projections of (small) precategories.

fredrik-bakke · 2023-09-28T15:02:32Z

src/category-theory/pullbacks-in-large-precategories.lagda.md

+  (g : hom-Large-Precategory C z x)
+  where
+
+  object-pullback-Large-Precategory : obj-Large-Precategory C l2


obj-pullback-...

fredrik-bakke · 2023-09-28T15:06:54Z

src/category-theory/pullbacks-in-large-precategories.lagda.md

+  object-pullback-Large-Precategory : obj-Large-Precategory C l2
+  object-pullback-Large-Precategory = pr1 (t x y z f g)
+
+  pr1-pullback-Large-Precategory :


Usually, I would want to say that you should take a look at foundation.pullbacks for how to name these. Sadly, that file is in need of refactoring as well. But you can have a look at foundation.cones-over-cospans for how to name these.

fredrik-bakke · 2023-09-28T15:11:20Z

src/category-theory/pullbacks-in-large-precategories.lagda.md

+    comp-hom-Large-Precategory C f p₁ ＝ comp-hom-Large-Precategory C g p₂ →
+    UU (α l1 ⊔ β l1 l1 ⊔ β l1 l2 ⊔ β l1 l3 ⊔ β l1 l4)
+  is-pullback-Large-Precategory x y z f g w p₁ p₂ _ =
+    (w' : obj-Large-Precategory C l1) →


w' must be able to live at any universe level

this should mirror the definition of universal-property-pullback in foundation-core.universal-property-pullbacks

Just to confirm your question earlier, using the above reference, x, y, z, and w should indeed all be able to have different universe levels.

fredrik-bakke · 2023-09-28T15:20:10Z

src/category-theory/pullbacks-in-large-precategories.lagda.md

+    (p₁' : hom-Large-Precategory C w' y) →
+    (p₂' : hom-Large-Precategory C w' z) →
+    comp-hom-Large-Precategory C f p₁' ＝ comp-hom-Large-Precategory C g p₂' →
+    ∃!


Instead of using unique existence, we prefer to define universal properties in terms of certain evaluation maps being equivalences. Here, that unfolds to requiring that the map that sends a morphism w' -> w, where w is the pullback, to the cone constructed by postcomposing with f and g being an iso in the (large) span precategory with fixed codomains y and z. Maybe Egbert has a different opinion on this, but that is what I would say this definition should be at the moment.

Maybe to expand a little on the above remark. Notice how this definition makes itself more readily available for use with univalence down the line.

I'm not sure I understand how this would be an isomorphism in the category of spans. Do you mean that postcomposition with f and g forms equivalence between the slice category C/w and the category of spans with codomains y and z?

Ah, yes, my bad, you're right!

Also, I shouldn't have said span category. It's the cone category over the cospan of f and g. And the cone is constructed by postcomposing with p and q, not f and g.

fredrik-bakke · 2023-09-28T15:25:39Z

src/category-theory/pullbacks-in-large-precategories.lagda.md

+  is-prop-is-pullback-Large-Precategory :
+    is-prop (is-pullback-Large-Precategory C x y z f g w p₁ p₂ α₁)
+  is-prop-is-pullback-Large-Precategory =
+    is-prop-Π³ (λ w' p₁' p₂' → is-prop-function-type is-property-is-contr)


Note that we are changing is-prop-Π³ to a general is-prop-iterated-Π 3 with #797 😁

fredrik-bakke · 2023-09-28T21:01:20Z

Do let me know if you have any questions about my comments!

fredrik-bakke · 2023-10-03T15:36:27Z

If this helps, they are currently working on formalizing elementary topoi over at 1lab. See in particular here for the subobject classifier: https://github.com/plt-amy/1lab/blob/e2c7a58fcf534c0611dd8bdea7d054f1eb80bd28/src/Cat/Diagram/Subobject.lagda.md, and note that they take a fibrational approach. Are you planning on taking a similar path? If so, that would be super neat! I was hoping to do some basic work on fibrations of categories at some point, but I don't currently know when/if I will take the time to do that.

EgbertRijke · 2023-10-20T10:41:24Z

Hi @maybemabeline! How is this PR going?

fredrik-bakke · 2023-10-31T07:19:20Z

That's too bad! Do get in touch if you want to coordinate on working towards formalizing this in the future, @maybemabeline. A little bit of topos theory wouldn't hurt the library :) I also did refactor pullbacks in types a bit in one of my recent PRs (#839), so that should give a better starting point now.

fredrik-bakke · 2023-10-31T07:23:01Z

No pressure though, there's an endless supply of cool things to formalize. 😄

Add pullbacks in large precategories

738a7eb

fredrik-bakke added the category-theory label Sep 28, 2023

fredrik-bakke reviewed Sep 28, 2023

View reviewed changes

src/category-theory/monomorphisms-in-large-precategories.lagda.md Outdated Show resolved Hide resolved

Add missing file

753b8ed

fredrik-bakke reviewed Sep 28, 2023

View reviewed changes

src/category-theory/pullbacks-in-large-precategories.lagda.md Outdated Show resolved Hide resolved

fredrik-bakke reviewed Sep 28, 2023

View reviewed changes

src/category-theory/pullbacks-in-large-precategories.lagda.md Outdated Show resolved Hide resolved

Update src/category-theory/pullbacks-in-large-precategories.lagda.md

8f2b187

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

fredrik-bakke reviewed Sep 28, 2023

View reviewed changes

maybemabeline added 2 commits September 29, 2023 10:53

Deindex variables and unnest module

92031c9

Reformat path algebra

bff8acd

maybemabeline closed this Oct 30, 2023

maybemabeline deleted the subobject-classifier branch November 1, 2023 09:10

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Subobject classifiers #802

Subobject classifiers #802

maybemabeline commented Sep 28, 2023

fredrik-bakke Sep 28, 2023 •

edited

Loading

fredrik-bakke Sep 28, 2023

fredrik-bakke Sep 28, 2023

maybemabeline Sep 28, 2023

fredrik-bakke Sep 28, 2023

fredrik-bakke Sep 28, 2023

fredrik-bakke Sep 28, 2023

fredrik-bakke Sep 28, 2023

fredrik-bakke Sep 28, 2023

fredrik-bakke Sep 28, 2023

fredrik-bakke Sep 28, 2023 •

edited

Loading

fredrik-bakke Sep 28, 2023 •

edited

Loading

fredrik-bakke Sep 28, 2023 •

edited

Loading

fredrik-bakke Sep 28, 2023

maybemabeline Sep 29, 2023

fredrik-bakke Sep 29, 2023

fredrik-bakke Sep 29, 2023

fredrik-bakke Sep 28, 2023

fredrik-bakke commented Sep 28, 2023

fredrik-bakke commented Oct 3, 2023

EgbertRijke commented Oct 20, 2023

fredrik-bakke commented Oct 31, 2023

fredrik-bakke commented Oct 31, 2023


		## Idea

		A pullback of two morphisms `f : hom y x` and `g : hom z x` in a category `C`

	A pullback of two morphisms `f : hom y x` and `g : hom z x` in a category `C`
	A pullback of two morphisms `f : hom y x` and `g : hom z x` in a [category](category-theory.categories.md) `C`

	We say that `C` has all pullbacks if there is a choice of a pullback for each
	We say that `C` has all pullbacks if there is a choice of a pullback for each

-    Σ (obj-Large-Precategory C l4) λ w →
-    Σ (hom-Large-Precategory C w y) λ p₁ →
-    Σ (hom-Large-Precategory C w z) λ p₂ →
-    Σ (comp-hom-Large-Precategory C f p₁
-    ＝ comp-hom-Large-Precategory C g p₂) λ α →
-      is-pullback-Large-Precategory x y z f g w p₁ p₂ α
+    Σ ( obj-Large-Precategory C l4)
+      ( λ w →
+        Σ ( hom-Large-Precategory C w y)
+          ( λ p →
+            Σ ( hom-Large-Precategory C w z)
+              ( λ q →
+                Σ ( comp-hom-Large-Precategory C f p ＝
+                    comp-hom-Large-Precategory C g q)
+                  ( is-pullback-Large-Precategory x y z f g w p q))))

Subobject classifiers #802

Subobject classifiers #802

Conversation

maybemabeline commented Sep 28, 2023

fredrik-bakke Sep 28, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fredrik-bakke Sep 28, 2023 • edited Loading

Choose a reason for hiding this comment

fredrik-bakke Sep 28, 2023 • edited Loading

Choose a reason for hiding this comment

fredrik-bakke Sep 28, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fredrik-bakke commented Sep 28, 2023

fredrik-bakke commented Oct 3, 2023

EgbertRijke commented Oct 20, 2023

fredrik-bakke commented Oct 31, 2023

fredrik-bakke commented Oct 31, 2023

fredrik-bakke Sep 28, 2023 •

edited

Loading

fredrik-bakke Sep 28, 2023 •

edited

Loading

fredrik-bakke Sep 28, 2023 •

edited

Loading

fredrik-bakke Sep 28, 2023 •

edited

Loading